(set-logic QF_UF)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-sort I 0)
(declare-fun op (I I) I)
(declare-fun e6 () I)
(declare-fun e5 () I)
(declare-fun e4 () I)
(declare-fun e3 () I)
(declare-fun e2 () I)
(declare-fun e1 () I)
(declare-fun e0 () I)
(assert 
  (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e0 e6)) (?v_7 (op e1 e0)) (?v_8 (op e1 e1)) (?v_9 (op e1 e2)) (?v_10 (op e1 e3)) (?v_11 (op e1 e4)) (?v_12 (op e1 e5)) (?v_13 (op e1 e6)) (?v_14 (op e2 e0)) (?v_15 (op e2 e1)) (?v_16 (op e2 e2)) (?v_17 (op e2 e3)) (?v_18 (op e2 e4)) (?v_19 (op e2 e5)) (?v_20 (op e2 e6)) (?v_21 (op e3 e0)) (?v_22 (op e3 e1)) (?v_23 (op e3 e2)) (?v_24 (op e3 e3)) (?v_25 (op e3 e4)) (?v_26 (op e3 e5)) (?v_27 (op e3 e6)) (?v_28 (op e4 e0)) (?v_29 (op e4 e1)) (?v_30 (op e4 e2)) (?v_31 (op e4 e3)) (?v_32 (op e4 e4)) (?v_33 (op e4 e5)) (?v_34 (op e4 e6)) (?v_35 (op e5 e0)) (?v_36 (op e5 e1)) (?v_37 (op e5 e2)) (?v_38 (op e5 e3)) (?v_39 (op e5 e4)) (?v_40 (op e5 e5)) (?v_41 (op e5 e6)) (?v_42 (op e6 e0)) (?v_43 (op e6 e1)) (?v_44 (op e6 e2)) (?v_45 (op e6 e3)) (?v_46 (op e6 e4)) (?v_47 (op e6 e5)) (?v_48 (op e6 e6))) (and (and (and (and (and (= ?v_0 e2) y) (or (or (= ?v_6 e2) (= ?v_6 e3)) (= ?v_6 e4))) (and (and (and (and (and (or (= ?v_14 e3) (= ?v_14 e6)) x) (= ?v_16 e2)) (= ?v_17 e6)) (or (= ?v_19 e4) (= ?v_19 e6))) (or (= ?v_20 e0) (= ?v_20 e6)))) (or (= ?v_27 e3) (= ?v_27 e5))) (= ?v_48 e6))))
(assert (and (and (= (op (op (op e2 e6) e6) e6) e2) (= (op (op (op e4 e6) e6) e6) e4)) (= (op (op (op e5 e6) e6) e6) e5)))
(assert 
  (let ((?v_0 (op e0 e0)) (?v_7 (op e0 e1)) (?v_14 (op e0 e2)) (?v_21 (op e0 e3)) (?v_28 (op e0 e4)) (?v_35 (op e0 e5)) (?v_42 (op e0 e6)) (?v_1 (op e1 e0)) (?v_8 (op e1 e1)) (?v_15 (op e1 e2)) (?v_22 (op e1 e3)) (?v_29 (op e1 e4)) (?v_36 (op e1 e5)) (?v_43 (op e1 e6)) (?v_2 (op e2 e0)) (?v_9 (op e2 e1)) (?v_16 (op e2 e2)) (?v_23 (op e2 e3)) (?v_30 (op e2 e4)) (?v_37 (op e2 e5)) (?v_44 (op e2 e6)) (?v_3 (op e3 e0)) (?v_10 (op e3 e1)) (?v_17 (op e3 e2)) (?v_24 (op e3 e3)) (?v_31 (op e3 e4)) (?v_38 (op e3 e5)) (?v_45 (op e3 e6)) (?v_4 (op e4 e0)) (?v_11 (op e4 e1)) (?v_18 (op e4 e2)) (?v_25 (op e4 e3)) (?v_32 (op e4 e4)) (?v_39 (op e4 e5)) (?v_46 (op e4 e6)) (?v_5 (op e5 e0)) (?v_12 (op e5 e1)) (?v_19 (op e5 e2)) (?v_26 (op e5 e3)) (?v_33 (op e5 e4)) (?v_40 (op e5 e5)) (?v_47 (op e5 e6)) (?v_6 (op e6 e0)) (?v_13 (op e6 e1)) (?v_20 (op e6 e2)) (?v_27 (op e6 e3)) (?v_34 (op e6 e4)) (?v_41 (op e6 e5)) (?v_48 (op e6 e6))) (and (and (not (= ?v_37 ?v_41)) (not (= ?v_39 ?v_40))) (not (= ?v_40 ?v_41)))))
(assert (= e6 (op e5 e0)))
(check-sat)
(exit)
